A, B:Type, f:(AB), l:A List. map(f;l)  B List 

latex

Definitions	t  T, x:A. B(x), A List, ||as||, i<j, b, ij, P  Q, False, A, AB, map(f;as), Prop, True, P  Q, T, , P & Q, P  Q
Lemmas	assert of lt int, bool wf, squash wf, true wf, map length, map wf, assert wf, lt int wf, length wf1, listp properties, listp wf